Left Termination of the query pattern
rem(g,a,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 189 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 75 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 7 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇒, 0 ms)
        ↳32 QDP
        ↳33 QDPOrderProof (⇔, 26 ms)
        ↳34 QDP
        ↳35 DependencyGraphProof (⇔, 0 ms)
        ↳36 TRUE
    ↳37 PiDP
        ↳38 UsableRulesProof (⇔, 0 ms)
        ↳39 PiDP
        ↳40 PiDPToQDPProof (⇒, 0 ms)
        ↳41 QDP
        ↳42 QDPSizeChangeProof (⇔, 0 ms)
        ↳43 YES

(0) Obligation:

Clauses:

rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
notZero(s(X)).
geq(s(X), s(Y)) :- geq(X, Y).
geq(X, 0).

Query: rem(g,a,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

subA(s(X1), s(X2), X3) :- subA(X1, X2, X3).
remB(s(X1), X2, X3) :- subE(X1, X2, X4).
remB(X1, X2, X3) :- ','(subcC(X1, X2, X4), remB(X4, X2, X3)).
remB(s(X1), X2, s(X1)) :- geqD(X1, X2).
subE(s(X1), s(X2), X3) :- subE(X1, X2, X3).
geqD(s(X1), s(X2)) :- geqD(X1, X2).
geqF(s(X1), s(X2)) :- geqF(X1, X2).
remH(s(X1), s(X2), X3) :- subA(X1, X2, X4).
remH(X1, s(X2), X3) :- ','(subcG(X1, X2, X4), remB(X4, X2, X3)).
remH(s(X1), s(X2), s(X1)) :- geqF(X1, X2).

Clauses:

subcA(s(X1), s(X2), X3) :- subcA(X1, X2, X3).
subcA(X1, 0, X1).
remcB(X1, X2, X3) :- ','(subcC(X1, X2, X4), remcB(X4, X2, X3)).
remcB(s(X1), X2, s(X1)) :- geqcD(X1, X2).
subcE(s(X1), s(X2), X3) :- subcE(X1, X2, X3).
subcE(X1, 0, X1).
geqcD(s(X1), s(X2)) :- geqcD(X1, X2).
geqcD(X1, 0).
geqcF(s(X1), s(X2)) :- geqcF(X1, X2).
geqcF(X1, 0).
subcG(s(X1), X2, X3) :- subcA(X1, X2, X3).
subcC(s(X1), X2, X3) :- subcE(X1, X2, X3).

Afs:

remH(x1, x2, x3)  =  remH(x1, x3)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
remH_in: (b,f,b)
subA_in: (b,f,f)
subcG_in: (b,f,f)
subcA_in: (b,f,f)
remB_in: (b,b,b)
subE_in: (b,b,f)
subcC_in: (b,b,f)
subcE_in: (b,b,f)
geqD_in: (b,b)
geqF_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

REMH_IN_GAG(s(X1), s(X2), X3) → U9_GAG(X1, X2, X3, subA_in_gaa(X1, X2, X4))
REMH_IN_GAG(s(X1), s(X2), X3) → SUBA_IN_GAA(X1, X2, X4)
SUBA_IN_GAA(s(X1), s(X2), X3) → U1_GAA(X1, X2, X3, subA_in_gaa(X1, X2, X3))
SUBA_IN_GAA(s(X1), s(X2), X3) → SUBA_IN_GAA(X1, X2, X3)
REMH_IN_GAG(X1, s(X2), X3) → U10_GAG(X1, X2, X3, subcG_in_gaa(X1, X2, X4))
U10_GAG(X1, X2, X3, subcG_out_gaa(X1, X2, X4)) → U11_GAG(X1, X2, X3, remB_in_ggg(X4, X2, X3))
U10_GAG(X1, X2, X3, subcG_out_gaa(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)
REMB_IN_GGG(s(X1), X2, X3) → U2_GGG(X1, X2, X3, subE_in_gga(X1, X2, X4))
REMB_IN_GGG(s(X1), X2, X3) → SUBE_IN_GGA(X1, X2, X4)
SUBE_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, subE_in_gga(X1, X2, X3))
SUBE_IN_GGA(s(X1), s(X2), X3) → SUBE_IN_GGA(X1, X2, X3)
REMB_IN_GGG(X1, X2, X3) → U3_GGG(X1, X2, X3, subcC_in_gga(X1, X2, X4))
U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → U4_GGG(X1, X2, X3, remB_in_ggg(X4, X2, X3))
U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)
REMB_IN_GGG(s(X1), X2, s(X1)) → U5_GGG(X1, X2, geqD_in_gg(X1, X2))
REMB_IN_GGG(s(X1), X2, s(X1)) → GEQD_IN_GG(X1, X2)
GEQD_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, geqD_in_gg(X1, X2))
GEQD_IN_GG(s(X1), s(X2)) → GEQD_IN_GG(X1, X2)
REMH_IN_GAG(s(X1), s(X2), s(X1)) → U12_GAG(X1, X2, geqF_in_ga(X1, X2))
REMH_IN_GAG(s(X1), s(X2), s(X1)) → GEQF_IN_GA(X1, X2)
GEQF_IN_GA(s(X1), s(X2)) → U8_GA(X1, X2, geqF_in_ga(X1, X2))
GEQF_IN_GA(s(X1), s(X2)) → GEQF_IN_GA(X1, X2)

The TRS R consists of the following rules:

subcG_in_gaa(s(X1), X2, X3) → U21_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(s(X1), s(X2), X3) → U14_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(X1, 0, X1) → subcA_out_gaa(X1, 0, X1)
U14_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcA_out_gaa(s(X1), s(X2), X3)
U21_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcG_out_gaa(s(X1), X2, X3)
subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subA_in_gaa(x1, x2, x3)  =  subA_in_gaa(x1)
subcG_in_gaa(x1, x2, x3)  =  subcG_in_gaa(x1)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x4)
subcA_in_gaa(x1, x2, x3)  =  subcA_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
subcA_out_gaa(x1, x2, x3)  =  subcA_out_gaa(x1, x2, x3)
subcG_out_gaa(x1, x2, x3)  =  subcG_out_gaa(x1, x2, x3)
remB_in_ggg(x1, x2, x3)  =  remB_in_ggg(x1, x2, x3)
subE_in_gga(x1, x2, x3)  =  subE_in_gga(x1, x2)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
geqD_in_gg(x1, x2)  =  geqD_in_gg(x1, x2)
geqF_in_ga(x1, x2)  =  geqF_in_ga(x1)
REMH_IN_GAG(x1, x2, x3)  =  REMH_IN_GAG(x1, x3)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)
SUBA_IN_GAA(x1, x2, x3)  =  SUBA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
U10_GAG(x1, x2, x3, x4)  =  U10_GAG(x1, x3, x4)
U11_GAG(x1, x2, x3, x4)  =  U11_GAG(x1, x2, x3, x4)
REMB_IN_GGG(x1, x2, x3)  =  REMB_IN_GGG(x1, x2, x3)
U2_GGG(x1, x2, x3, x4)  =  U2_GGG(x1, x2, x3, x4)
SUBE_IN_GGA(x1, x2, x3)  =  SUBE_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)
U4_GGG(x1, x2, x3, x4)  =  U4_GGG(x1, x2, x3, x4)
U5_GGG(x1, x2, x3)  =  U5_GGG(x1, x2, x3)
GEQD_IN_GG(x1, x2)  =  GEQD_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U12_GAG(x1, x2, x3)  =  U12_GAG(x1, x3)
GEQF_IN_GA(x1, x2)  =  GEQF_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REMH_IN_GAG(s(X1), s(X2), X3) → U9_GAG(X1, X2, X3, subA_in_gaa(X1, X2, X4))
REMH_IN_GAG(s(X1), s(X2), X3) → SUBA_IN_GAA(X1, X2, X4)
SUBA_IN_GAA(s(X1), s(X2), X3) → U1_GAA(X1, X2, X3, subA_in_gaa(X1, X2, X3))
SUBA_IN_GAA(s(X1), s(X2), X3) → SUBA_IN_GAA(X1, X2, X3)
REMH_IN_GAG(X1, s(X2), X3) → U10_GAG(X1, X2, X3, subcG_in_gaa(X1, X2, X4))
U10_GAG(X1, X2, X3, subcG_out_gaa(X1, X2, X4)) → U11_GAG(X1, X2, X3, remB_in_ggg(X4, X2, X3))
U10_GAG(X1, X2, X3, subcG_out_gaa(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)
REMB_IN_GGG(s(X1), X2, X3) → U2_GGG(X1, X2, X3, subE_in_gga(X1, X2, X4))
REMB_IN_GGG(s(X1), X2, X3) → SUBE_IN_GGA(X1, X2, X4)
SUBE_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, subE_in_gga(X1, X2, X3))
SUBE_IN_GGA(s(X1), s(X2), X3) → SUBE_IN_GGA(X1, X2, X3)
REMB_IN_GGG(X1, X2, X3) → U3_GGG(X1, X2, X3, subcC_in_gga(X1, X2, X4))
U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → U4_GGG(X1, X2, X3, remB_in_ggg(X4, X2, X3))
U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)
REMB_IN_GGG(s(X1), X2, s(X1)) → U5_GGG(X1, X2, geqD_in_gg(X1, X2))
REMB_IN_GGG(s(X1), X2, s(X1)) → GEQD_IN_GG(X1, X2)
GEQD_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, geqD_in_gg(X1, X2))
GEQD_IN_GG(s(X1), s(X2)) → GEQD_IN_GG(X1, X2)
REMH_IN_GAG(s(X1), s(X2), s(X1)) → U12_GAG(X1, X2, geqF_in_ga(X1, X2))
REMH_IN_GAG(s(X1), s(X2), s(X1)) → GEQF_IN_GA(X1, X2)
GEQF_IN_GA(s(X1), s(X2)) → U8_GA(X1, X2, geqF_in_ga(X1, X2))
GEQF_IN_GA(s(X1), s(X2)) → GEQF_IN_GA(X1, X2)

The TRS R consists of the following rules:

subcG_in_gaa(s(X1), X2, X3) → U21_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(s(X1), s(X2), X3) → U14_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(X1, 0, X1) → subcA_out_gaa(X1, 0, X1)
U14_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcA_out_gaa(s(X1), s(X2), X3)
U21_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcG_out_gaa(s(X1), X2, X3)
subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subA_in_gaa(x1, x2, x3)  =  subA_in_gaa(x1)
subcG_in_gaa(x1, x2, x3)  =  subcG_in_gaa(x1)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x4)
subcA_in_gaa(x1, x2, x3)  =  subcA_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
subcA_out_gaa(x1, x2, x3)  =  subcA_out_gaa(x1, x2, x3)
subcG_out_gaa(x1, x2, x3)  =  subcG_out_gaa(x1, x2, x3)
remB_in_ggg(x1, x2, x3)  =  remB_in_ggg(x1, x2, x3)
subE_in_gga(x1, x2, x3)  =  subE_in_gga(x1, x2)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
geqD_in_gg(x1, x2)  =  geqD_in_gg(x1, x2)
geqF_in_ga(x1, x2)  =  geqF_in_ga(x1)
REMH_IN_GAG(x1, x2, x3)  =  REMH_IN_GAG(x1, x3)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)
SUBA_IN_GAA(x1, x2, x3)  =  SUBA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
U10_GAG(x1, x2, x3, x4)  =  U10_GAG(x1, x3, x4)
U11_GAG(x1, x2, x3, x4)  =  U11_GAG(x1, x2, x3, x4)
REMB_IN_GGG(x1, x2, x3)  =  REMB_IN_GGG(x1, x2, x3)
U2_GGG(x1, x2, x3, x4)  =  U2_GGG(x1, x2, x3, x4)
SUBE_IN_GGA(x1, x2, x3)  =  SUBE_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)
U4_GGG(x1, x2, x3, x4)  =  U4_GGG(x1, x2, x3, x4)
U5_GGG(x1, x2, x3)  =  U5_GGG(x1, x2, x3)
GEQD_IN_GG(x1, x2)  =  GEQD_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U12_GAG(x1, x2, x3)  =  U12_GAG(x1, x3)
GEQF_IN_GA(x1, x2)  =  GEQF_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 16 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GEQF_IN_GA(s(X1), s(X2)) → GEQF_IN_GA(X1, X2)

The TRS R consists of the following rules:

subcG_in_gaa(s(X1), X2, X3) → U21_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(s(X1), s(X2), X3) → U14_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(X1, 0, X1) → subcA_out_gaa(X1, 0, X1)
U14_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcA_out_gaa(s(X1), s(X2), X3)
U21_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcG_out_gaa(s(X1), X2, X3)
subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subcG_in_gaa(x1, x2, x3)  =  subcG_in_gaa(x1)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x4)
subcA_in_gaa(x1, x2, x3)  =  subcA_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
subcA_out_gaa(x1, x2, x3)  =  subcA_out_gaa(x1, x2, x3)
subcG_out_gaa(x1, x2, x3)  =  subcG_out_gaa(x1, x2, x3)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
GEQF_IN_GA(x1, x2)  =  GEQF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GEQF_IN_GA(s(X1), s(X2)) → GEQF_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
GEQF_IN_GA(x1, x2)  =  GEQF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GEQF_IN_GA(s(X1)) → GEQF_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GEQF_IN_GA(s(X1)) → GEQF_IN_GA(X1)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GEQD_IN_GG(s(X1), s(X2)) → GEQD_IN_GG(X1, X2)

The TRS R consists of the following rules:

subcG_in_gaa(s(X1), X2, X3) → U21_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(s(X1), s(X2), X3) → U14_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(X1, 0, X1) → subcA_out_gaa(X1, 0, X1)
U14_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcA_out_gaa(s(X1), s(X2), X3)
U21_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcG_out_gaa(s(X1), X2, X3)
subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subcG_in_gaa(x1, x2, x3)  =  subcG_in_gaa(x1)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x4)
subcA_in_gaa(x1, x2, x3)  =  subcA_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
subcA_out_gaa(x1, x2, x3)  =  subcA_out_gaa(x1, x2, x3)
subcG_out_gaa(x1, x2, x3)  =  subcG_out_gaa(x1, x2, x3)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
GEQD_IN_GG(x1, x2)  =  GEQD_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GEQD_IN_GG(s(X1), s(X2)) → GEQD_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GEQD_IN_GG(s(X1), s(X2)) → GEQD_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GEQD_IN_GG(s(X1), s(X2)) → GEQD_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBE_IN_GGA(s(X1), s(X2), X3) → SUBE_IN_GGA(X1, X2, X3)

The TRS R consists of the following rules:

subcG_in_gaa(s(X1), X2, X3) → U21_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(s(X1), s(X2), X3) → U14_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(X1, 0, X1) → subcA_out_gaa(X1, 0, X1)
U14_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcA_out_gaa(s(X1), s(X2), X3)
U21_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcG_out_gaa(s(X1), X2, X3)
subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subcG_in_gaa(x1, x2, x3)  =  subcG_in_gaa(x1)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x4)
subcA_in_gaa(x1, x2, x3)  =  subcA_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
subcA_out_gaa(x1, x2, x3)  =  subcA_out_gaa(x1, x2, x3)
subcG_out_gaa(x1, x2, x3)  =  subcG_out_gaa(x1, x2, x3)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
SUBE_IN_GGA(x1, x2, x3)  =  SUBE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBE_IN_GGA(s(X1), s(X2), X3) → SUBE_IN_GGA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUBE_IN_GGA(x1, x2, x3)  =  SUBE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUBE_IN_GGA(s(X1), s(X2)) → SUBE_IN_GGA(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUBE_IN_GGA(s(X1), s(X2)) → SUBE_IN_GGA(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REMB_IN_GGG(X1, X2, X3) → U3_GGG(X1, X2, X3, subcC_in_gga(X1, X2, X4))
U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)

The TRS R consists of the following rules:

subcG_in_gaa(s(X1), X2, X3) → U21_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(s(X1), s(X2), X3) → U14_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(X1, 0, X1) → subcA_out_gaa(X1, 0, X1)
U14_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcA_out_gaa(s(X1), s(X2), X3)
U21_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcG_out_gaa(s(X1), X2, X3)
subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subcG_in_gaa(x1, x2, x3)  =  subcG_in_gaa(x1)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x4)
subcA_in_gaa(x1, x2, x3)  =  subcA_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
subcA_out_gaa(x1, x2, x3)  =  subcA_out_gaa(x1, x2, x3)
subcG_out_gaa(x1, x2, x3)  =  subcG_out_gaa(x1, x2, x3)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
REMB_IN_GGG(x1, x2, x3)  =  REMB_IN_GGG(x1, x2, x3)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REMB_IN_GGG(X1, X2, X3) → U3_GGG(X1, X2, X3, subcC_in_gga(X1, X2, X4))
U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)

The TRS R consists of the following rules:

subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
REMB_IN_GGG(x1, x2, x3)  =  REMB_IN_GGG(x1, x2, x3)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REMB_IN_GGG(X1, X2, X3) → U3_GGG(X1, X2, X3, subcC_in_gga(X1, X2))
U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)

The TRS R consists of the following rules:

subcC_in_gga(s(X1), X2) → U22_gga(X1, X2, subcE_in_gga(X1, X2))
U22_gga(X1, X2, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)
subcE_in_gga(s(X1), s(X2)) → U18_gga(X1, X2, subcE_in_gga(X1, X2))
subcE_in_gga(X1, 0) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)

The set Q consists of the following terms:

subcC_in_gga(x0, x1)
U22_gga(x0, x1, x2)
subcE_in_gga(x0, x1)
U18_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U3_GGG(X1, X2, X3, subcC_out_gga(X1, X2, X4)) → REMB_IN_GGG(X4, X2, X3)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(REMB_IN_GGG(x1, x2, x3)) = x1   
POL(U18_gga(x1, x2, x3)) = x3   
POL(U22_gga(x1, x2, x3)) = 1 + x3   
POL(U3_GGG(x1, x2, x3, x4)) = x4   
POL(s(x1)) = 1 + x1   
POL(subcC_in_gga(x1, x2)) = x1   
POL(subcC_out_gga(x1, x2, x3)) = 1 + x3   
POL(subcE_in_gga(x1, x2)) = x1   
POL(subcE_out_gga(x1, x2, x3)) = x3   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

subcC_in_gga(s(X1), X2) → U22_gga(X1, X2, subcE_in_gga(X1, X2))
subcE_in_gga(s(X1), s(X2)) → U18_gga(X1, X2, subcE_in_gga(X1, X2))
subcE_in_gga(X1, 0) → subcE_out_gga(X1, 0, X1)
U22_gga(X1, X2, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)
U18_gga(X1, X2, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REMB_IN_GGG(X1, X2, X3) → U3_GGG(X1, X2, X3, subcC_in_gga(X1, X2))

The TRS R consists of the following rules:

subcC_in_gga(s(X1), X2) → U22_gga(X1, X2, subcE_in_gga(X1, X2))
U22_gga(X1, X2, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)
subcE_in_gga(s(X1), s(X2)) → U18_gga(X1, X2, subcE_in_gga(X1, X2))
subcE_in_gga(X1, 0) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)

The set Q consists of the following terms:

subcC_in_gga(x0, x1)
U22_gga(x0, x1, x2)
subcE_in_gga(x0, x1)
U18_gga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(36) TRUE

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBA_IN_GAA(s(X1), s(X2), X3) → SUBA_IN_GAA(X1, X2, X3)

The TRS R consists of the following rules:

subcG_in_gaa(s(X1), X2, X3) → U21_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(s(X1), s(X2), X3) → U14_gaa(X1, X2, X3, subcA_in_gaa(X1, X2, X3))
subcA_in_gaa(X1, 0, X1) → subcA_out_gaa(X1, 0, X1)
U14_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcA_out_gaa(s(X1), s(X2), X3)
U21_gaa(X1, X2, X3, subcA_out_gaa(X1, X2, X3)) → subcG_out_gaa(s(X1), X2, X3)
subcC_in_gga(s(X1), X2, X3) → U22_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(s(X1), s(X2), X3) → U18_gga(X1, X2, X3, subcE_in_gga(X1, X2, X3))
subcE_in_gga(X1, 0, X1) → subcE_out_gga(X1, 0, X1)
U18_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcE_out_gga(s(X1), s(X2), X3)
U22_gga(X1, X2, X3, subcE_out_gga(X1, X2, X3)) → subcC_out_gga(s(X1), X2, X3)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
subcG_in_gaa(x1, x2, x3)  =  subcG_in_gaa(x1)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x4)
subcA_in_gaa(x1, x2, x3)  =  subcA_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
subcA_out_gaa(x1, x2, x3)  =  subcA_out_gaa(x1, x2, x3)
subcG_out_gaa(x1, x2, x3)  =  subcG_out_gaa(x1, x2, x3)
subcC_in_gga(x1, x2, x3)  =  subcC_in_gga(x1, x2)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
subcE_in_gga(x1, x2, x3)  =  subcE_in_gga(x1, x2)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
0  =  0
subcE_out_gga(x1, x2, x3)  =  subcE_out_gga(x1, x2, x3)
subcC_out_gga(x1, x2, x3)  =  subcC_out_gga(x1, x2, x3)
SUBA_IN_GAA(x1, x2, x3)  =  SUBA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBA_IN_GAA(s(X1), s(X2), X3) → SUBA_IN_GAA(X1, X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUBA_IN_GAA(x1, x2, x3)  =  SUBA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUBA_IN_GAA(s(X1)) → SUBA_IN_GAA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUBA_IN_GAA(s(X1)) → SUBA_IN_GAA(X1)
    The graph contains the following edges 1 > 1

(43) YES